protocol race_OverlappingMultiOut {
child:
    async Msg1();
    async Msg1_();
    async __delete__(); suppressUndeleteableError();

parent:
    async Msg2();
    async Msg2_();


start state _:
    send __delete__;
    send suppressUndeleteableError goto S10;

    // *** ERROR: send/recv of Msg1/Msg2 in state S10 goes to overlapping
    // sets { S11, S12 }, { S12, S13 } and thus can't be unidirectional
state S10:
    send Msg1 goto S11 or S12;
    recv Msg2 goto S12 or S13;

state S11:
    recv Msg2 goto S14;

state S12:
    send Msg1 goto S14;
    recv Msg2 goto S14;

state S13:
    send Msg1 goto S14;

state S14:
    send Msg1 goto S14;
    recv Msg2 goto S14;
};
